$\forall$$A$, $B$:Type. $A$ $\subseteq\rho$ $B$ $\Rightarrow$ ($\forall$$x$, $y$:$A$. $x$ $=$ $y$ $\in$ $B$ $\Rightarrow$ $x$ $=$ $y$) $\Rightarrow$ EqDecider($B$) $\subseteq$ EqDecider($A$)